\begin{tabbing}
$\vdash$  \=$\forall$$T$:Type, $L$:($T$ List), $P$:(\{$x$:$T$$\mid$ ($x$ $\in$ $L$)\} $\rightarrow\mathbb{P}$).\+
\\[0ex]($\forall$$x$$\in$$L$. Dec($P$($x$))) $\Rightarrow$ ($\exists$${\it L'}$:$T$ List. (${\it L'}$ $\subseteq$ $L$ \& ($\forall$$x$:$T$. ($x$ $\in$ ${\it L'}$) $\Leftarrow\!\Rightarrow$ (($x$ $\in$ $L$) \& $P$($x$)))))
\-
\end{tabbing}